In this section we prove that termination is decidable for \hof processes.
As hinted at in the introduction, this is in sharp contrast with the analogous result for \hocore.
The proof appeals to the theory of well-structured transition systems, whose main definitions and results we summarize next.

\subsection{Well-Structured Transition Systems}\label{ss:wsts}
%\paragraph{\bf Well-Structured Transition Systems.}
The following results and definitions are from \citep{FinkelS01},  unless
differently specified. Recall that a \emph{quasi-order} (or, equivalently, preorder) is a reflexive
and transitive relation.

\begin{mydefi}[Well-quasi-order]
A \emph{well-quasi-order} (wqo) is a quasi-order $\leq$ over a
set $X$ such that, for any infinite sequence $x_0 , x_1 , x_2 \ldots \in X$, there exist indexes $i < j$
such that $x_i \leq x_j$.
\end{mydefi}

  Note that if $\leq$ is a wqo then any infinite sequence $x_0 , x_1 , x_2 , \ldots$ contains an infinite
increasing subsequence $x_{i_0} , x_{i_1} , x_{i_2} , \ldots$ (with $i_0 < i_1 < i_2 < \ldots$). 
Thus well-quasi-orders exclude the possibility of having infinite strictly decreasing sequences.


We also need a definition for (finitely branching) transition systems. This can
be given as follows. Here and in the following %$\rightarrow^{+}$ (resp. 
$\rightarrow^*$ denotes the 
%transitive (resp. the 
reflexive and transitive
%) 
closure of the relation $\rightarrow$.


\begin{mydefi}[Transition system]
A \emph{transition system} is a structure $TS = (S, \rightarrow)$, where $S$ is a set of states
and $\rightarrow \subseteq  S \times S$ is a set of transitions. 
We define $Succ(s)$ as the set $\{s' \in S \mid s \rightarrow s' \}$
of immediate successors of $S$. We say that $TS$ is finitely branching if, for each $s \in S$,
$Succ(s)$ is finite.
%We also define $Pred(s)$ as the set $\{s' \in S \mid s' \rightarrow s\}$ of immediate predecessors of $s$,
%while $Pred^*(s)$ denotes the set $\{s \in S \mid s' \rightarrow^* s\}$ (of predecessors of $s$).
\end{mydefi}




The function $Succ$ %$Pred$ and $Pred^*$ 
will also be used  on sets by assuming 
%that in this case they are defined by 
the point-wise extension of the above definitions.
%
 The key tool to decide several properties of computations is the notion of \emph{well-structured
transition system}. This is a transition system equipped with a well-quasi-order on states
which is (upward) compatible with the transition relation. Here we will use a strong version 
of compatibility; hence the following definition.


\begin{mydefi}[Well-structured transition system] %with strong compatibility]
A \emph{well-structured transition system with strong compatibility} is a transition system 
$TS = (S, \rightarrow)$, equipped with a quasi-order $\leq$ on $S$, such that the two following conditions hold:
\vspace{-2mm}
\begin{enumerate}
\item $\leq$ is a well-quasi-order;
\item $\leq$ is strongly (upward) compatible with $\rightarrow$, that is, for all $s_1 \leq t_1$ and all transitions
    $s_1 \rightarrow s_2$ , there exists a state $t_2$ such that $t_1 \rightarrow t_2$ and $s_2 \leq t_2$ holds.
\end{enumerate}
\end{mydefi}

The following theorem is a special case of Theorem 4.6 in \citep{FinkelS01} and will be used to obtain our decidability result.

\begin{theorem}\label{th:Finkel}
Let $TS = (S, \rightarrow, \leq)$ be a finitely branching, well-structured transition
system with strong compatibility, decidable $\leq$,  and computable $Succ$. Then the existence
of an infinite computation starting from a state $s \in S$ is decidable.
\end{theorem}

We will also need a result due to \cite{Higman52} which allows to extend a well-quasi-order
from a set $S$ to the set of the finite sequences on $S$. More precisely, given a set $S$ let
us denote by $S^*$ the set of finite sequences built by using elements in $S$. 
We can define a quasi-order on $S^*$ as follows.

\begin{mydefi}\label{def:eqwqo}
Let $S$ be a set and $\leq$ a quasi-order over $S$. The relation $\leq_*$ over $S^*$
is defined as follows. Let $t, u \in S^*$, with $t = t_1 t_2 \ldots t_m$ and $u = u_1 u_2 \ldots u_n$. 
We have that $t \leq_* u$ if and only if there exists an injection $f$ from $\{1, 2, \ldots m \}$ 
to $\{1, 2, \ldots n\}$ such that $t_i \leq u_{f (i)}$ and $i \leq f (i)$ for $
i = 1, \ldots , m$.
\end{mydefi}

The relation $\leq_*$ is clearly a quasi-order over $S^*$. 
It is also a wqo, since we have the following result.

\begin{lemma}[\cite{Higman52}] 
\label{lem:Higman}
Let $S$ be a set and $\leq$ a wqo over $S$. 
Then %the relation 
$\leq_*$ is a wqo over $S^*$.
\end{lemma}

Finally we will use also the following proposition, whose proof is immediate.

\begin{proposition}\label{prop:eqwqo}
Let $S$ be a finite set. Then the equality is a wqo over $S$.
\end{proposition}